3(1(x1)) → 4(1(x1))
5(9(x1)) → 2(6(5(x1)))
3(5(x1)) → 8(9(7(x1)))
9(x1) → 3(2(3(x1)))
8(4(x1)) → 6(x1)
2(6(x1)) → 4(3(x1))
3(8(x1)) → 3(2(7(x1)))
9(x1) → 5(0(2(x1)))
8(8(4(x1))) → 1(9(x1))
7(1(x1)) → 6(9(x1))
3(9(x1)) → 9(3(x1))
7(5(x1)) → 1(0(x1))
↳ QTRS
↳ DependencyPairsProof
3(1(x1)) → 4(1(x1))
5(9(x1)) → 2(6(5(x1)))
3(5(x1)) → 8(9(7(x1)))
9(x1) → 3(2(3(x1)))
8(4(x1)) → 6(x1)
2(6(x1)) → 4(3(x1))
3(8(x1)) → 3(2(7(x1)))
9(x1) → 5(0(2(x1)))
8(8(4(x1))) → 1(9(x1))
7(1(x1)) → 6(9(x1))
3(9(x1)) → 9(3(x1))
7(5(x1)) → 1(0(x1))
51(9(x1)) → 51(x1)
31(8(x1)) → 71(x1)
91(x1) → 21(x1)
31(5(x1)) → 81(9(7(x1)))
91(x1) → 21(3(x1))
31(8(x1)) → 31(2(7(x1)))
31(8(x1)) → 21(7(x1))
31(9(x1)) → 91(3(x1))
81(8(4(x1))) → 91(x1)
31(9(x1)) → 31(x1)
31(5(x1)) → 71(x1)
21(6(x1)) → 31(x1)
71(1(x1)) → 91(x1)
91(x1) → 51(0(2(x1)))
51(9(x1)) → 21(6(5(x1)))
91(x1) → 31(2(3(x1)))
91(x1) → 31(x1)
31(5(x1)) → 91(7(x1))
3(1(x1)) → 4(1(x1))
5(9(x1)) → 2(6(5(x1)))
3(5(x1)) → 8(9(7(x1)))
9(x1) → 3(2(3(x1)))
8(4(x1)) → 6(x1)
2(6(x1)) → 4(3(x1))
3(8(x1)) → 3(2(7(x1)))
9(x1) → 5(0(2(x1)))
8(8(4(x1))) → 1(9(x1))
7(1(x1)) → 6(9(x1))
3(9(x1)) → 9(3(x1))
7(5(x1)) → 1(0(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
51(9(x1)) → 51(x1)
31(8(x1)) → 71(x1)
91(x1) → 21(x1)
31(5(x1)) → 81(9(7(x1)))
91(x1) → 21(3(x1))
31(8(x1)) → 31(2(7(x1)))
31(8(x1)) → 21(7(x1))
31(9(x1)) → 91(3(x1))
81(8(4(x1))) → 91(x1)
31(9(x1)) → 31(x1)
31(5(x1)) → 71(x1)
21(6(x1)) → 31(x1)
71(1(x1)) → 91(x1)
91(x1) → 51(0(2(x1)))
51(9(x1)) → 21(6(5(x1)))
91(x1) → 31(2(3(x1)))
91(x1) → 31(x1)
31(5(x1)) → 91(7(x1))
3(1(x1)) → 4(1(x1))
5(9(x1)) → 2(6(5(x1)))
3(5(x1)) → 8(9(7(x1)))
9(x1) → 3(2(3(x1)))
8(4(x1)) → 6(x1)
2(6(x1)) → 4(3(x1))
3(8(x1)) → 3(2(7(x1)))
9(x1) → 5(0(2(x1)))
8(8(4(x1))) → 1(9(x1))
7(1(x1)) → 6(9(x1))
3(9(x1)) → 9(3(x1))
7(5(x1)) → 1(0(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
31(8(x1)) → 71(x1)
91(x1) → 21(x1)
31(5(x1)) → 81(9(7(x1)))
91(x1) → 21(3(x1))
31(8(x1)) → 31(2(7(x1)))
31(8(x1)) → 21(7(x1))
31(9(x1)) → 91(3(x1))
81(8(4(x1))) → 91(x1)
31(9(x1)) → 31(x1)
31(5(x1)) → 71(x1)
21(6(x1)) → 31(x1)
71(1(x1)) → 91(x1)
91(x1) → 31(2(3(x1)))
91(x1) → 31(x1)
31(5(x1)) → 91(7(x1))
3(1(x1)) → 4(1(x1))
5(9(x1)) → 2(6(5(x1)))
3(5(x1)) → 8(9(7(x1)))
9(x1) → 3(2(3(x1)))
8(4(x1)) → 6(x1)
2(6(x1)) → 4(3(x1))
3(8(x1)) → 3(2(7(x1)))
9(x1) → 5(0(2(x1)))
8(8(4(x1))) → 1(9(x1))
7(1(x1)) → 6(9(x1))
3(9(x1)) → 9(3(x1))
7(5(x1)) → 1(0(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
31(5(x1)) → 81(9(7(x1)))
81(8(4(x1))) → 91(x1)
Used ordering: Polynomial interpretation [25,35]:
31(8(x1)) → 71(x1)
91(x1) → 21(x1)
91(x1) → 21(3(x1))
31(8(x1)) → 31(2(7(x1)))
31(8(x1)) → 21(7(x1))
31(9(x1)) → 91(3(x1))
31(9(x1)) → 31(x1)
31(5(x1)) → 71(x1)
21(6(x1)) → 31(x1)
71(1(x1)) → 91(x1)
91(x1) → 31(2(3(x1)))
91(x1) → 31(x1)
31(5(x1)) → 91(7(x1))
The value of delta used in the strict ordering is 1/2.
POL(5(x1)) = 1
POL(31(x1)) = 1
POL(9(x1)) = 1
POL(4(x1)) = 0
POL(8(x1)) = 4
POL(71(x1)) = 1
POL(1(x1)) = 0
POL(21(x1)) = 1
POL(7(x1)) = 0
POL(3(x1)) = (4)x_1
POL(81(x1)) = (1/2)x_1
POL(2(x1)) = 0
POL(6(x1)) = 0
POL(91(x1)) = 1
POL(0(x1)) = 0
3(1(x1)) → 4(1(x1))
3(5(x1)) → 8(9(7(x1)))
8(4(x1)) → 6(x1)
3(9(x1)) → 9(3(x1))
3(8(x1)) → 3(2(7(x1)))
9(x1) → 3(2(3(x1)))
2(6(x1)) → 4(3(x1))
8(8(4(x1))) → 1(9(x1))
9(x1) → 5(0(2(x1)))
7(1(x1)) → 6(9(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
31(8(x1)) → 71(x1)
91(x1) → 21(x1)
91(x1) → 21(3(x1))
31(8(x1)) → 31(2(7(x1)))
31(8(x1)) → 21(7(x1))
31(9(x1)) → 91(3(x1))
31(9(x1)) → 31(x1)
31(5(x1)) → 71(x1)
21(6(x1)) → 31(x1)
71(1(x1)) → 91(x1)
91(x1) → 31(2(3(x1)))
91(x1) → 31(x1)
31(5(x1)) → 91(7(x1))
3(1(x1)) → 4(1(x1))
5(9(x1)) → 2(6(5(x1)))
3(5(x1)) → 8(9(7(x1)))
9(x1) → 3(2(3(x1)))
8(4(x1)) → 6(x1)
2(6(x1)) → 4(3(x1))
3(8(x1)) → 3(2(7(x1)))
9(x1) → 5(0(2(x1)))
8(8(4(x1))) → 1(9(x1))
7(1(x1)) → 6(9(x1))
3(9(x1)) → 9(3(x1))
7(5(x1)) → 1(0(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
51(9(x1)) → 51(x1)
3(1(x1)) → 4(1(x1))
5(9(x1)) → 2(6(5(x1)))
3(5(x1)) → 8(9(7(x1)))
9(x1) → 3(2(3(x1)))
8(4(x1)) → 6(x1)
2(6(x1)) → 4(3(x1))
3(8(x1)) → 3(2(7(x1)))
9(x1) → 5(0(2(x1)))
8(8(4(x1))) → 1(9(x1))
7(1(x1)) → 6(9(x1))
3(9(x1)) → 9(3(x1))
7(5(x1)) → 1(0(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
51(9(x1)) → 51(x1)
The value of delta used in the strict ordering is 8.
POL(9(x1)) = 4 + (4)x_1
POL(51(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
3(1(x1)) → 4(1(x1))
5(9(x1)) → 2(6(5(x1)))
3(5(x1)) → 8(9(7(x1)))
9(x1) → 3(2(3(x1)))
8(4(x1)) → 6(x1)
2(6(x1)) → 4(3(x1))
3(8(x1)) → 3(2(7(x1)))
9(x1) → 5(0(2(x1)))
8(8(4(x1))) → 1(9(x1))
7(1(x1)) → 6(9(x1))
3(9(x1)) → 9(3(x1))
7(5(x1)) → 1(0(x1))